Type soundness

In computer science, a programming language with a static type system is considered to be type sound if a well-typed program cannot cause type errors.[1] If an expression is assigned type t, and it evaluates to a value v, then v is in the set of values defined by t. SML, OCAML, Scheme and Ada have sound type systems. Most implementations of C and C++ do not.

See also

References

  1. ^ Adrew K. Wright and Matthias Felleisen (June 18, 1992), A Syntactic Approach to Type Soundness, Rice Technical Report TR91-160, Department of Computer Science, Rice University.